*****∀E cause2 Do(Pat,Tell(Joe,Tm)),Know(Joe,Tm),w;

1 (true(w,Occur Do(Pat,Tell(Joe,Tm)))∧true(w,Cause(Do(Pat,Tell(Joe,Tm)),Know(Joe,Tm))))⊃true(w,Future Know(Joe,T%
m))  

*****∀E tell1 Pat,Joe,Tm,w;

2 true(w,Know(Pat,Tm))⊃true(w,Cause(Do(Pat,Tell(Joe,Tm)),Know(Joe,Tm)))  

*****∀E logic3 Know(Pat,Tm),Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm),w;

3 true(w,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm)))≡(true(w,Know(Pat,Tm))⊃tr%
ue(w,Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm)))  

*****∀E logic3 Occur Do(Pat,Tell(Joe,Tm)),Future Know(Joe,Tm),w;

4 true(w,Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm))≡(true(w,Occur Do(Pat,Tell(Joe,Tm)))⊃true(w,Futu%
re Know(Joe,Tm)))  

*****TAUT true(w,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm))) 1:↑;

5 true(w,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm)))  

*****∀I ↑ w;

6 ∀w.true(w,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm)))  

*****∀E nec Pat,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm));

7 ∀w.true(w,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm)))⊃∀w.true(w,K(Pat,Know(%
Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm))))  

*****⊃E ↑↑,↑;

8 ∀w.true(w,K(Pat,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm))))  

*****∀E ↑ world;

9 true(world,K(Pat,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm))))  

*****∀E introspection1 Pat,Tm,world;

10 true(world,Know(Pat,Tm))⊃true(world,K(Pat,Know(Pat,Tm)))  

*****∀E introspection5 Pat,Know(Pat,Tm),Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm),world;

11 (true(world,K(Pat,Know(Pat,Tm)))∧true(world,K(Pat,Know(Pat,Tm) Implies (Occur Do(Pat,Tell(Joe,Tm)) Implies Fu%
ture Know(Joe,Tm)))))⊃true(world,K(Pat,Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm)))  

*****∀E wantdo Pat,Know(Joe,Tm),Tell(Joe,Tm),world;

12 (true(world,Want(Pat,Know(Joe,Tm)))∧true(world,K(Pat,Occur Do(Pat,Tell(Joe,Tm)) Implies Future Know(Joe,Tm)))%
)⊃true(world,Occur Do(Pat,Tell(Joe,Tm)))  

*****∀E tell1 Pat,Joe,Tm,world;

13 true(world,Know(Pat,Tm))⊃true(world,Cause(Do(Pat,Tell(Joe,Tm)),Know(Joe,Tm)))  

*****∀E cause2 Do(Pat,Tell(Joe,Tm)),Know(Joe,Tm),world;

14 (true(world,Occur Do(Pat,Tell(Joe,Tm)))∧true(world,Cause(Do(Pat,Tell(Joe,Tm)),Know(Joe,Tm))))⊃true(world,Futu%
re Know(Joe,Tm))  

*****TAUT true(world,Future Know(Joe,Tm)) problem11,problem12,9:↑;

15 true(world,Future Know(Joe,Tm))